1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
use super::*;
#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
pub struct SubstSlice<V, T = ()> {
substs: V,
base: u32,
ctx: T,
}
impl<V> SubstSlice<V> {
pub fn new(substs: V, base: u32) -> SubstSlice<V> {
SubstSlice {
substs,
base,
ctx: (),
}
}
}
impl<V, T, B> SubstSlice<V, T>
where
T: TyCtxMut,
V: Deref<Target = [B]>,
B: Borrow<TermId>,
{
pub fn new_with(substs: V, base: u32, mut ctx: T) -> Result<SubstSlice<V, T>, Error> {
for (i, s) in substs.iter().enumerate() {
if let Some(annot) = s.borrow().annot() {
let ty = &*annot.get_ty_id(ctx.cons_ctx());
if !ctx.constrain(i as u32 + base, ty)?.unwrap_or(true) {
return Err(Error::TypeMismatch);
}
}
}
Ok(SubstSlice { substs, base, ctx })
}
}
impl<V, T, B> SubstCtx for SubstSlice<V, T>
where
V: Deref<Target = [B]>,
T: TyCtxMut,
B: Borrow<TermId>,
{
type Ctx = T::MaxDeref;
#[inline]
fn subst_var(&mut self, ix: u32, annot: Option<&TermId>) -> Result<Option<TermId>, Error> {
if let Some(subst_ix) = ix.checked_sub(self.base) {
let substs = &*self.substs;
if (subst_ix as usize) < substs.len() {
let subst: &B = &substs[substs.len() - 1 - subst_ix as usize];
Ok(Some(subst.borrow().clone()))
} else {
let ty = annot.subst_rec(self)?;
let new_ix = ix - self.substs.len() as u32;
if ty.is_none() && new_ix == ix {
return Ok(None);
}
let ty = ty
.unwrap_or_else(|| annot.consed(self.ctx.cons_ctx()))
.map(|ty| ty.into_shallow_cons(self.ctx.cons_ctx()));
let term = Var::new_unchecked(new_ix, ty).into_id_with(self.ctx.cons_ctx());
Ok(Some(term))
}
} else if let Some(Some(ty)) = annot.subst_rec(self)? {
Ok(Some(Var::with_ty(ix, ty).into_id_with(self.ctx.cons_ctx())))
} else {
Ok(None)
}
}
#[inline]
fn push_param(&mut self, param_ty: Option<&TermId>) -> Result<Option<TermId>, Error> {
let subst = if let Some(param_ty) = param_ty {
param_ty.subst_id(self)?
} else {
None
};
self.ctx.push_param(subst.as_ref().or(param_ty))?;
self.base += 1;
Ok(subst)
}
#[inline]
fn intersects(&self, filter: VarFilter, _code: Code, _form: Form) -> bool {
filter.fvb() >= self.base
}
#[inline]
fn ctx(&mut self) -> &mut Self::Ctx {
self.ctx.ctx()
}
#[inline]
fn pop_param(&mut self) -> Result<(), Error> {
self.ctx.pop_param()?;
self.base -= 1;
Ok(())
}
#[inline]
fn is_var_null(&self) -> bool {
self.substs.as_ref().is_empty()
}
}